from sklearn.svm import SVC
from z3 import *
import numpy as np
from sklearn.model_selection import train_test_split
from sklearn.preprocessing import StandardScaler

# 定义约束条件
def define_constraints(x, y):
    constraints = [
        x + y >= 10,  # 示例约束：x + y 至少为10
        x <= y         # 示例约束：x 必须小于等于 y
    ]
    return constraints

# 模拟训练数据
def generate_training_data():
    # 生成一些输入数据
    X = np.random.rand(100, 2) * 20
    # 生成对应的标签，这里假设输入 (x, y) 满足 x + y >= 10 为正类，否则为负类
    y = (X[:, 0] + X[:, 1] >= 10).astype(int)
    return X, y

# 训练SVM模型
def train_svm(X, y):
    scaler = StandardScaler()
    X_scaled = scaler.fit_transform(X)
    X_train, X_test, y_train, y_test = train_test_split(X_scaled, y, test_size=0.2, random_state=42)
    svm = SVC(kernel='linear', C=1.0)
    svm.fit(X_train, y_train)
    return svm, scaler

# 生成测试用例
def generate_test_cases(svm, scaler, num_cases):
    cases = []
    while len(cases) < num_cases:
        # 随机生成测试用例
        x = np.random.rand(2) * 20
        scaled_x = scaler.transform([x])
        # 检查是否属于正类
        if svm.predict(scaled_x)[0] == 1:
            # 验证是否满足约束
            s = Solver()
            s.add(define_constraints(IntVal(x[0]), IntVal(x[1])))
            if s.check() == sat:
                cases.append(x)
    return cases

# 主程序
if __name__ == "__main__":
    # 生成训练数据
    X, y = generate_training_data()
    # 训练SVM模型
    svm, scaler = train_svm(X, y)
    # 生成测试用例
    test_cases = generate_test_cases(svm, scaler, 10)
    print("Generated Test Cases:", test_cases)